COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out) 
C00012 ENDMK
C⊗;
(wipe-out) 
(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

;1
(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
(bindingpower: 950))

;2
(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
(bindingpower: 950))

;3
(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

;4
(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

;5
(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

;6
(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

;7
(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

;8
(decl (u v w) (type: |ground|) (sort: |listp|))

;9
(decl (x y z) (type: |ground|) (sort: |sexp|))

;10
(decl (xa ya za) (type: |ground|) (sort: |atom|))

;11
(decl (phi) (type: |ground→truthval|))

;12
(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
(prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info
 
;13
(axiom |∀xa.sexp(xa)|)
(label simpinfo)

;14
(axiom |∀u.sexp u|)
(label simpinfo)

;15
(axiom |∀x u.listp x.u|)
(label simpinfo)

;16
(axiom |∀u.¬null u ⊃ listp cdr u|)
(label simpinfo)

;17
(axiom |∀u.¬null u ⊃ sexp car u|)
(label simpinfo)

;18
(axiom |∀x.¬atom x ⊃ sexp car x|)
(label simpinfo)

;19
(axiom |∀x.¬atom x ⊃ sexp cdr x|)
(label simpinfo)

;20
(axiom |∀x y.sexp x.y|)
(label simpinfo)

;21
(axiom |∀x y.¬atom x.y|)
(label simpinfo)

;22
(axiom |∀x u.¬null x.u|)
(label simpinfo)

;23
(axiom |∀u.null u ⊃ u = nil|)
(label simpinfo)

;24
(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

;25
(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

;26
(axiom |car nil = nil|)
(label simpinfo)

;27
(axiom |cdr nil = nil|)
(label simpinfo)

;28
(axiom |∀u.¬null u ⊃ (car u.cdr u=u)|)
(label simpinfo) (label cons_car_cdr)

;29
(axiom |∀x.¬atom x ⊃ (car x.cdr x=x)|)
(label simpinfo) (label cons_car_cdr)

;;;induction

;30
(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)
;31
(decl pars (type: |ground*|))

;32
(decl (df df1 df2) (type: |ground⊗ground*→ground*|))

;33
(decl nilcase (type: |ground*→ground*|))

;34
(axiom
|∀df nilcase def.(∃fun.(∀pars x u.fun(nil,pars)=nilcase(pars)∧
                               fun(x.u,pars)=def(x,u,fun(u,df(x,pars)),pars)))|)
(label listinductiondef)

;35
(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

;36
(axiom
|∀atomcase defsexp df1 df2.
∃fun. ∀pars x y z.
(atom z ⊃ fun(z,pars)=atomcase(z,pars))∧
(fun(x.y,pars)=defsexp(x,y,fun(x,df1(x,y,pars)),fun(y,df2(x,y,pars)),pars))|)
(label sexpinductiondef)

;a high order definition schema when above is insufficient

;37
(decl (arb arb1 arb2) (type: |?arbitrary|))

;38
(decl bigfun (type: |ground⊗ground⊗@arb⊗@arb→@arb|))

;39
(decl (defined_fun atom_fun) (type: |ground→@arb|))

;this is the primitive recursive schema for definition on  ALL
;higher type functionals:
;note the use of the variable type in declarations;
;in this way we can specialize to ANY type.

;40
(axiom
|∀bigfun atom_fun.∃defined_fun.∀x y.(atom x ⊃ defined_fun(x)=atom_fun(x))∧
                                 (defined_fun(x.y)=
                                   bigfun(x,y,defined_fun(x),defined_fun(y)))|)
(label high_order_definition)
 
;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

;41
(decl list (type: |ground* → ground|) (syntype: constant))

;42
(decl lst (type: |ground*|))

;43
(axiom |list() = nil|)
(label simpinfo)

;44
(axiom |∀lst.listp(list(lst))|)
(label simpinfo)

;45
(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)
(label listdef)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
;46
(decl append (type: |ground⊗ground⊗(ground*)→ground|) (syntype: constant)
  (associativity: both) (infixname: **) (bindingpower: 840))

;47
(defax append |∀x u v.nil**v=v∧(x.u)**v=x.(u**v)|)
(label appendef) (label simpinfo)

;48
(axiom |∀u v.listp(u**v)|)
(label simpinfo) (label listappend)

;49
(axiom |∀u.u**nil=u|)
(label simpinfo)

;50
(axiom |∀x v.(x.nil)**v=x.v|)
(label simpinfo)

;;;map functions on lists

;51
(decl (allp somep) (syntype: constant) (type: |(@phi)⊗ground→truthval|))

;52
(defax allp |∀phi x u.allp(phi,nil)∧
                  allp(phi,x.u)=if phi(x) then allp(phi,u) else false|)
(label allpdef)

;53
(defax somep |∀phi x u.¬somep(phi,nil)∧
                   somep(phi,x.u)=if phi(x) then true else somep(phi,u)|)
(label somepdef)

;54
(defax mapcar |∀fn x u.mapcar(fn,nil)=nil∧mapcar(fn,x.u)=fn(x).mapcar(fn,u)|)
(label mapcardef)

;55
(decl (alist) (type: ground) (sort: alistp))

;56
(axiom |∀alist. listp alist|)
(label simpinfo) 

;57
(axiom |∀u.alistp u ≡ (¬null u ⊃
                       ¬atom car u∧atom car (car u)∧alistp(cdr u))|)
(label alistdef1)

;58
(axiom |∀xa y alist.alistp nil ∧ alistp (xa.y).alist|)
(label alistdef) (label simpinfo)

;59
(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

;60
(defax assoc |∀x xa y alist.
          assoc(x,nil)=nil∧
          assoc(x,(xa.y).alist)=(if x=xa then xa.y else assoc(x,alist))|)
(label assocdef)

;61
(axiom |∀x alist.sexp assoc(x,alist)|)
(label simpinfo)

;62
(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

;63
(defax member |∀x y u. ¬member(x,nil)∧member(x,y.u)=(x=y∨member(x,u))|)
(label memberdef)

;64
(decl uniqueness (type: |ground → truthval|) (syntype: constant))

;65
(defax uniqueness |∀u x.uniqueness nil∧
                        (uniqueness(x.u)≡¬member(x,u)∧uniqueness u)|)
(label uniquenessdef)

;66
(ue (phi |λu.sexp car(u)|) listinduction)
(label simpinfo)

;67
(ue (phi |λu.listp cdr(u)|) listinduction)
(label simpinfo)

(save-proofs lispax)